DS($A$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it sort}$:($A$$\rightarrow$Type) $\times$ ($a$:$A$$\rightarrow$EqDecider(${\it sort}$($a$)))